package edu.ut.ece382c.valloy.translator.tester;

import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.LinkedList;
import java.util.Vector;

import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.parser.Module;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;
import edu.ut.ece382c.valloy.translator.engine.ParserTranslator;
import edu.ut.ece382c.valloy.translator.engine.Translator;
import edu.ut.ece382c.valloy.translator.engine.StringTranslator;

public class ValloyTestDriver {

	public File rootDir;	//holds base path
	private File[] files;	//holds all files found within a directory
	private TestLogger out;
	private StringBuilder outputString;
	private Translator translator ;
	
	//TestSuiteLevels:
	//0: Type-check and compile all models
	//1: Default. Additionally, run all commands and check satisfiability. Compare against original model when failures are suspected
	//2: Same as above but all command results are compared against original command results
	public int testSuiteLevel;

	//Constructors
	public ValloyTestDriver(File rootDir) {
		this.rootDir = rootDir;
		this.outputString = new StringBuilder();    
		this.out = new TestLogger(outputString);
		this.translator = new ParserTranslator ();
		this.testSuiteLevel = 1;
	}
	
	public ValloyTestDriver() {
		this.rootDir = null;
		this.outputString = new StringBuilder();    
		this.out = new TestLogger(outputString);
		this.translator = new ParserTranslator ();
		this.testSuiteLevel = 1;
	}
	

	//Main: Takes a path to the root folder to recursively search for models
	//feeds those models to Alloy or VAlloy analyzer to check that they compile
	static public void main (String[] root) {
		
		ValloyTestDriver driver = new ValloyTestDriver (new File(root[0]));
		driver.out.enableConsoleOut(true);
		if (root.length>1)        
			driver.testSuiteLevel = ( root[1] !=null)? Integer.valueOf(root[1]) : 0;
		
		driver.RunTestDrive(driver.rootDir.getPath());
	}
	
	public TestLogger getLogger (){
		return out;
	}

	public void setTranslator (Translator translator){
		this.translator = translator;
	}
	
	public void setTestSuiteLevel (int level){
		this.testSuiteLevel= level;
	}
	
	public String RunTestDrive(String root){
		long suiteTime = System.currentTimeMillis(); 
		out.append("************************************************************************\n" +
					"* Starting Test-Sutie\n" +
					"************************************************************************\n");

		out.appendLn ("* Base path: " + root);
		out.appendLn ("* Parser Type: " + translator.getClass().getCanonicalName());
		out.appendLn ("* Checking Level: " + ((testSuiteLevel>0)?"Compile & Run":"Compile Only"));
		out.appendLn ("************************************************************************");

		rootDir = new File(root); //Create test driver and point to root
		
		Vector<File> models = FindModels();	//Find all models at or below root
        
        
		A4Reporter rep = new A4Reporter() {
            // For example, here we choose to display each "warning" by printing it to System.out
            @Override public void warning(ErrorWarning msg) {
            	out.append("Relevance Warning:\n"+(msg.toString().trim())+"\n\n");
            }
        };
		
		class Issue {
			public File model = null;
			public Err error = null;
			public Exception exc = null;
		    public Issue(File model, Err error) {
		        this.model = model;
		        this.error = error;
		    }
		    public Issue(File model, Exception Exc) {
		        this.model = model;
		        this.exc = Exc;
		    }
		}
		
		//Create the desired translation engine
		Translator TestedTranslator = null;
		TestedTranslator = translator;
		
		Vector<Issue> failures = new Vector<Issue>();
		long modelTime;
		for (File originalModel : models){
			modelTime = System.currentTimeMillis();
			//System.out.print(model.getPath() + "\n");
            File testModel = new File(originalModel.getPath().replaceAll("\\.als|\\.vls", ".test.txt"));
            FileWriter tempWriter = null;

            out.appendLn("************************************************************************\n" +
						"Translating "+ originalModel.getName() + " to " + testModel.getName());
            try {
            	
	            tempWriter = new FileWriter(testModel);
				tempWriter.write(TestedTranslator.TranslateModule(originalModel));
				tempWriter.close();
			}
            catch (Err error){
            	out.appendLn("Error while translating: " + originalModel.getName() +
            			"\nAt: " + error.pos.toString() + "\n" +
            			error.getMessage());
            	if (originalModel.getName().endsWith(".vls_error"))
            		out.appendLn("Errors are expected for " + originalModel.getName() +
            					"\nTest is OK");
				else
					failures.add(new Issue(testModel, error));
            	try {
					tempWriter.close();
					testModel.delete();
				} catch (IOException e) {
					//ignore close errors
				}
            	continue;
            }			
            catch (Exception Exc){
            	out.append("Error while translating: " + originalModel.getName() + "\"" +
            	Exc.getMessage() + "\n");
            	if (originalModel.getName().endsWith(".vls_error"))
            		out.appendLn("Errors are expected for " + originalModel.getName() +
            					"\nTest is OK");
				else
					failures.add(new Issue(testModel, Exc));
            	try {
					tempWriter.close();
					testModel.delete();
				} catch (IOException e) {
					//ignore close errors
				}
            	continue;
            }
            
            out.appendLn("Parsing+Typechecking: "+ testModel.getName());
            try {
                Module translated = CompUtil.parseEverything_fromFile(rep, null, testModel.getPath());
                
                if (testSuiteLevel>0){
	                A4Options options = new A4Options();
	                options.solver = A4Options.SatSolver.SAT4J;
	                long commandTime;
	                for (Command command: translated.getAllCommands()) {
	                    // Execute the command
	                	commandTime = System.currentTimeMillis();
	                	out.append("*----------------------------------------------------------------------*\n" +
	                    					"Executing command \""+command+"\" in " + testModel.getName() + "\n");
	                    A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, translated.getAllReachableSigs(), command, options);
	                    // Print the outcome
	                    out.appendLn(ans.satisfiable()?"Satisfiable":"Unsatisfiable");
	                    //System.out.println("Alloy's detailed answer:");
	                    //System.out.println(ans);
	                    if (testSuiteLevel>0){
	                    	boolean inconsistency;
	                    	if ((command.expects == -1) && (command.check ^ ans.satisfiable()) ) //we are probably OK if these are different ( XOR is TRUE)																 //and no expected answer is specified
	                    		inconsistency=false;
	                    	else {
	                    		inconsistency = ((command.expects == 1) ^ ans.satisfiable()); //TRUE means that we didn't get the expected result
	                    	}			
	                    	if (inconsistency) {
	                    		out.appendLn("Found possible inconsistency: " 
		                    				+ (command.check?"\"Check\"":"\"Run\"")
                    						+ " command for which "
                    						+ (command.check?"there is a counterexample":"no instance was found"));
	                    		if (originalModel.getName().endsWith(".vls"))
     		                    	throw (new Exception("Possible change of meaning with command \"" + command + "\" in " + testModel.getName()));	                    			
	                    		else{	
		                    		out.appendLn("\nChecking original model...");
	                    	
			                    	// this is a workaround to try to free up some memory to avoid Java's out of heap errors
			                    	boolean ansSatisfied = ans.satisfiable(); //remember whether the command under test was satisfied
			                    	ans= null;	//try to free up some memory
			                    	//java.lang.Runtime.getRuntime().gc(); //garbage-collect!
			                    	
			                    	Module original = CompUtil.parseEverything_fromFile(rep, null, originalModel.getPath());
			                    	
			                    	boolean commandFound=false; //make sure we can match the tested command with the original command
			                    	for (Command originalCommand: original.getAllCommands()) {
			        	                if (originalCommand.toString().contentEquals(command.toString())){
			        	                	 A4Solution originalSolution = TranslateAlloyToKodkod.execute_command(rep, original.getAllReachableSigs(), originalCommand, options);
			        	                	 if (ansSatisfied  ^ originalSolution.satisfiable()) //if answers don't match
			        	                	 {
			     		                    	throw (new Exception("Possible change of meaning with command \"" + command + "\" in " + testModel.getName()));
			        	                	 }
			        	                	 else {
			        	                		 out.append("Original model has the same behavior\n");
			        	                		 out.append("Command \"" + command + "\" is OK\n\n");
			        	                	 }
			        	                	 commandFound = true;
			        	                }
			                    	}
			                    	if (!commandFound){
			                        	throw (new Exception("Was not able to find command \"" + command.toString() + "\" in original model"));
			                    	}
	                    		}
		                    }
	                    	else
	                    		out.append("Command \"" + command + "\" is OK\n\n");
	                    }
                    commandTime = System.currentTimeMillis() - commandTime;
                    out.append ("Command execution time: " + commandTime/1000 + " seconds\n");
	                }
                testModel.delete();
                }
                else	//if below level 1
                	testModel.delete();               
            }
            catch (Err error){
            	out.append("Error while compiling: " + originalModel.getName() + ":\n" + error.msg + "\n\n");
            	if (originalModel.getName().endsWith(".vls_error"))
            		out.appendLn("Errors are expected for " + originalModel.getName() +
            					"\nTest is OK");
				else
            		failures.add(new Issue(testModel,error));
            }
            catch (Exception Exc){
            	if (originalModel.getName().endsWith(".vls_error"))
            		out.appendLn("Errors are expected for " + originalModel.getName() +
            					"Error:\n" + Exc.getMessage() + "\n");
            	else
                	out.appendLn(Exc.getMessage() + "\n");
            		failures.add(new Issue(testModel, Exc));
            }
        modelTime = System.currentTimeMillis() - modelTime;
        out.append ("Model check time: " + modelTime/1000 + " seconds\n");
		}
		
		out.append("#########################################################################\n");
		out.append("Checked " + models.size() + " model" +(models.size()>1?"s\n":"\n"));
		
		if (failures.size()>0){
			out.append(failures.size() + " Problem" + ((failures.size()>1)?"s":"") + " found:\n" );
			int counter = 1;
			for (Issue problem: failures ){
	        	if (problem.error != null){
	        		out.append("Problem #" + counter++ + ":\n" +	     
	        					"Error while compiling translated output: " + problem.model.getName() + ":\n" + 
	        					"At: " + problem.error.pos.toString() + "\n" +
	        					problem.error.msg + "\n" + 
	        					"-----------------------------------------------------\n");
	        	}
	        	if (problem.exc != null){
	        		out.append("Problem #" + counter++ + ":\n" +
	        					"Exception while while translating: " + problem.model.getName() + ":\n" + 
	        					problem.exc.getMessage() + "\n" + 
	        					"-----------------------------------------------------\n");
	        	}
	        }
		}
		else {
			out.append("No Errors Found\n");
			
		}
        suiteTime = System.currentTimeMillis() - suiteTime;
        out.append ("Total test-suite time: " + suiteTime/1000 + " seconds\n");
        out.append("#########################################################################\n");
		return out.flush();
	}
	
	
	//recursive search for models
	private Vector<File> FindModels (){
		LinkedList<File> directories = new LinkedList<File>();
		Vector<File> models  = new Vector<File>();
		directories.add(rootDir);

		while (!(directories.isEmpty())){
			files = directories.remove().listFiles();
			for (File file : files){
				if (file.isDirectory()){
					directories.addLast(file);
					//System.out.print ("dir found: " + file.getName()+ "\n");
				}
				else if (file.getName().endsWith(".als") || file.getName().endsWith(".vls") || file.getName().endsWith(".vls_error")  ){
					models.addElement(file);
					out.append("found model: " + file.getName() + "\n");
				}
			}
		}
	return models;
	}
}
